Inference at * 1 0 
Iof proof for Lemma sq stable iff:



1. P : 
2. Q : 
3. SqStable(P)
4. SqStable(Q)
  SqStable(P  Q) 

latex

 by PERMUTE{1:n, 2:n, 3:n, 4:n, 5:n, 4:n, 3:n, 6:n} 

latex

 1: .....wf..... NILNIL

 1:   (P  Q)  
 2: .....wf..... NILNIL

 2:   (Q  P)  
 3: .....wf..... NILNIL

 3:   P  
 4: .....wf..... NILNIL

 4:   Q  
 5: 

 5:   SqStable(Q)
 6: 

 6:   SqStable(P)
 .

Definitions	t  T, f(a), s = t, x:AB(x), P  Q, SqStable(P), , x:A. B(x), P  Q, P  Q, P  Q
Lemmas	sq stable implies, sq stable and